home
***
CD-ROM
|
disk
|
FTP
|
other
***
search
/
Turnbull China Bikeride
/
Turnbull China Bikeride - Disc 1.iso
/
ARGONET
/
PD
/
PROGRAMMING
/
LCLINT2.SPK
/
test
/
test_b
/
c
/
null6
< prev
next >
Wrap
Text File
|
1996-08-28
|
1KB
|
84 lines
typedef /*@null@*/ int *mnull;
extern /*@notnull@*/ mnull mnull_create (void);
extern int f1 (/*@notnull@*/ mnull x); /* 1. Function f1 declared with notnull ... */
int f (mnull x)
{
return *x; /* 2. Possible dereference of null pointer: *x */
}
static /*@unused@*/ int f2 (/*@notnull@*/ mnull x)
{
return *x;
}
extern /*@falsenull@*/ bool isThree (mnull x);
static /*@unused@*/ int f3 (/*@notnull@*/ mnull x)
{
if (isThree)
{
*x = 4;
}
else
{
*x = 5;
}
return (*x);
}
/*@notnull@*/ mnull f4 (void)
{
mnull x = NULL;
if (x == NULL)
{
x = mnull_create ();
}
return x;
}
/*@notnull@*/ mnull f5 (void)
{
static /*@only@*/ mnull x = NULL;
if (x == NULL)
{
x = mnull_create ();
}
return x;
}
/*@notnull@*/ mnull f6 (void)
{
static /*@only@*/ mnull x = NULL;
if (x != NULL)
{
x = mnull_create ();
}
return x; /* 3. Possibly null storage returned as non-null */
}
/*@notnull@*/ mnull f7 (void)
{
static /*@only@*/ mnull x = NULL;
if (x == NULL)
{
x = mnull_create ();
}
else
{
x = NULL;
}
return x; /* 4. Possibly null storage returned as non-null */
}